package server.sat;

import java.security.MessageDigest;
import java.security.NoSuchAlgorithmException;
import java.util.ArrayList;
import java.util.Comparator;
import java.util.List;
import java.util.Scanner;
import java.util.concurrent.Callable;

import server.core.Problem;

/**
 * The SATProblemParser class defines an object that parses CNF data from a
 * string, producing a {@link SATProblem} as a result.
 * 
 * @author Clayton Edward Taylor
 */
public class SATProblemParser implements Callable<Problem> {

	private String data;
	
	/**
	 * Creates a new SATProblemParser that will parse the given data.
	 * 
	 * @param data - The CNF data to parse
	 * @see          SATProblemParser
	 */
	public SATProblemParser(String data) {
		
		this.data = data;
	}
	
	/**
	 * Parses the given data, producing a {@link SATProblem} object.
	 * 
	 * @return The SATProblem for the given data
	 * @see    SATProblemParser
	 */
	@Override
	public Problem call() throws Exception {
		
		String sortedProblem = sortProblem(data);
		String hashedProblem = hashProblem(sortedProblem);
		
		return new SATProblem(hashedProblem, sortedProblem);
	}
	
	/**
	 * Takes the pre-processed CNF data and produces a hash for it to be used
	 * as the key for the problem.
	 * 
	 * @param data - The pre-processed CNF data
	 * @return       A hash of the problem data
	 * @see          SATProblemParser
	 */
	private String hashProblem(String data) {
		
		MessageDigest md;
		try {
			md = MessageDigest.getInstance("SHA-256");
		} catch (NoSuchAlgorithmException e) {
			throw new RuntimeException(e);
		}
		md.update(data.getBytes());
		byte[] byteData = md.digest();
		StringBuilder sb = new StringBuilder(byteData.length * 2);
		for (byte b : byteData) {
			sb.append(String.format("%02x", b & 0xff));
		}
		return sb.toString();
	}
	
	/**
	 * Takes a CNF problem and sorts the variables within each clause and then
	 * the clauses themselves to ensure that the same problem always yields the
	 * same hash.
	 * 
	 * @param data - The original CNF problem data
	 * @return       The sorted CNF problem data
	 * @see          SATProblemParser
	 */
	private String sortProblem(String data) {
		
		Scanner parser = new Scanner(data);
		String headerLine = readHeaderLine(parser);
		List<List<Integer>> clauses = tokenizeProblem(parser);
		sortClauses(clauses);
		
		StringBuilder sb = new StringBuilder(headerLine + "\n");
		for (List<Integer> c : clauses) {
			for (int v : c) {
				sb.append(v);
				sb.append(" ");
			}
			sb.append("0\n");
		}
		
		return sb.toString();
	}
	
	/**
	 * Extracts the header line from the CNF problem (ignoring all comment 
	 * lines in the process).
	 * 
	 * @param parser - The Scanner that contains the CNF data
	 * @return         The header line for the CNF problem
	 * @see            SATProblemParser
	 */
	private String readHeaderLine(Scanner parser) {
		
		String headerLine;
		do {
			headerLine = parser.nextLine().trim();;
		} while (!headerLine.startsWith("p"));
		
		return headerLine;
	}
	
	/**
	 * Tokenizes the clauses of the CNF problem data by representing each
	 * variable as an Integer and each clause as a List<Integer>.
	 * 
	 * @param parser - The Scanner that contains the CNF data with the comment
	 *                 and header lines extracted
	 * @return         The clauses of the CNF problem
	 * @see            SATProblemParser
	 */
	private List<List<Integer>> tokenizeProblem(Scanner parser) {
		
		List<List<Integer>> clauses = new ArrayList<List<Integer>>();
		List<Integer> c = new ArrayList<Integer>();
		while (parser.hasNextInt()) {
			int v = parser.nextInt();
			if (v == 0) {
				clauses.add(c);
				c = new ArrayList<Integer>();
			} else {
				c.add(v);
			}
		}
		
		return clauses;
	}
	
	/**
	 * Sorts the variables within each clause and then the clauses themselves.
	 * 
	 * @param clauses - The clauses to be sorted
	 * @see             SATProblemParser
	 */
	private void sortClauses(List<List<Integer>> clauses) {
		
		for (List<Integer> c : clauses) {
			java.util.Collections.sort(c);
		}
		java.util.Collections.sort(clauses, new ClauseComparator());
	}
	
	/**
	 * The ClauseComparator class defines an implementation of the Comparator
	 * interface for List<Integer> so that the clauses can be sorted using the
	 * <code>sort</code> method of Collections class.
	 * 
	 * @see SATProblemParser
	 */
	private class ClauseComparator implements Comparator<List<Integer>> {

		@Override
		public int compare(List<Integer> c1, List<Integer> c2) {
			
			int minLength = Math.min(c1.size(), c2.size());
			for (int i = 0; i < minLength; ++i) {
				int v1 = c1.get(i);
				int v2 = c2.get(i);
				if (v1 != v2) {
					return v1 - v2;
				}
			}
			return c1.size() - c2.size();
		}
	}
}
